T:Type, eq:EqDecider(T), d1, d2:a:T fp Type.
AtomFree(d1)  AtomFree(d2)  AtomFree(d1  d2) 

latex

Definitions	False, P  Q, A, left+right, P  Q, b, x:A. B(x), t  T, b, , s = t, Prop, Type, x.A(x), x. t(x), Top, a:A fp B(a), x:AB(x), x  dom(f), x:AB(x), P & Q, P  Q, Unit, Void, x:A. B(x), f  g, AtomFree(T;x), xdom(f). v=f(x)   P(x;v), EqDecider(T), {x:A| B(x) }, x,y. t(x;y), AtomFree(d)
Lemmas	fpf-all wf, atom-free wf, fpf wf, deq wf, fpf-join wf, top wf, fpf-join-dom, fpf-join-ap-sq, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, fpf-dom wf, fpf-trivial-subtype-top, bool wf, bnot wf, not wf, assert wf